g, h:GrpSig, f:MonHom(g,h).
fun_thru_1op(|g|;|h|;~;~;f)  Inj(|g|;|h|;f)  Inverse(|h|;*;e;~)  Inverse(|g|;*;e;~) 

latex

Up	groups 1
Definitions of Statement	IsMonHom{M1,M2}(f), MonHom(M1,M2)
Definitions	t  T, Inverse(T;op;id;inv), P  Q, x:A. B(x), P  Q, P  Q, P & Q, x f y, FunThru2op(A;B;opa;opb;f), IsMonHom{M1,M2}(f), Inj(A;B;f), fun_thru_1op(A;B;opa;opb;f), MonHom(M1,M2),
Lemmas	grp sig wf, monoid hom wf, fun thru 1op wf, inject wf, grp inv wf, grp id wf, grp op wf, inverse wf, grp car wf, monoid hom properties